Nuprl Lemma : bor_tt_simp 9,38

u:. (u tt) = tt   
latex


ProofTree


Definitionst  T
Lemmasbool wf, btrue wf

origin